\documentclass{article}\usepackage{noweb}\pagestyle{noweb}\noweboptions{}\begin{document}\nwfilename{construct_bdd.snw}\nwbegindocs{0}%    construct_bdd.snw% ===> this file was generated automatically by noweave --- better not edit it
%    
%    Description:  This is a stand-alone program to construct a
%    Reduced order Binary Decision diagram. It is written in
%    literate style. 
%    
%    Version:  1.0
%    Created:  Wednesday 03 August 2011 08:26:02  IST
%   Revision:  none
%   Compiler:  gcc
%
%     Author:  (c) 2011, Dilawar Singh, dilawar@ee.iitb.ac.in
%  Institute:  Indian Institute of Technology Bombay
% 
%% RELEASED UNDER GNU-GPL

\title{Binary Decision Diagrams}
\author{Dilawar Singh}
\maketitle
\section{Introduction}
 
Reduced Order Binary  Decision  Diagrams  (ROBDD),  usually  called  Binary
decision Diagrams  (BDD),  is  a  propotional  directed  acyclic  graph  (a
data-structure) which can be used to represent a boolean function.   For  a
given ordering of variables, representation of a boolean function in  terms
of a BDD is guarenteed to be unique \ref{Byrant}

In this implementation, we want to create a BDD. The expression or function
or propotional logic is given to  us  in  a  txt  file  with  a  particular
ordering on variables.  The ordering of variables in very  important  since
size of the BDD for a  given  function  depends  on  the  ordering  of  the
variables.  We should  read  this  file  and  save  it  in  an  appropriate
data-structure.


We plan to use  Standaard  template  libraries  (STL).   It  provides  some
advanced data-structures with  many  pre-defined  functions  to  manipulate
them.    All   include    file    will    appear    {\Tt{}IncludesHeaderFiles\nwendquote}


\section{The data-structure}

Binary Decision Diagram (BDD) essentially are \textbf{binary decision dag},
a binary tree with shared binary tree, a directed acyclic graph (dag) in
which exactly two distinguished arcs emanate from every non-sink node.

In computer memory, a bdd node can is represented like following.

\begin{verbatim}
        --------------------------------------
        |            |           |           |
        |    V       |   LO      |    HI     |
        |            |           |           |
        --------------------------------------
\end{verbatim}
where 'V' holds the name (or index) of the variable, 'LO' and 'HI' are
pointer to another node or sink.

BDD has two properties. It is \textbf{ordered} i.e. if a LO or HI node from
\textcircled{i} points to another node \textcircled{j} then $i \le j$.
Thus, in particular, no variable $x_j$ will ever be queried twice when
function is evaluted.  Also BDD must be \textbf{reduced} in the sense that
it does not waste space. This means that branch node's LO and HI must never
be equal, and no two nodes in BDD representation should have same triple of
value(V, LO, HI).

So basically, a BDD is a abstract liked list with some constrained specified on
them.

\subsection{Implementation of data-structure}


\subsection{The BDD file}

User should pass  BDD expression in a text file with a variable ordering.
If a variable ordering is not given then a ordering is derived by looking
at the order in which variable appears in the BDD expression. BDD
expression can be nested.

Following are the characer codes for logical function.

\begin{verbatim}
            && ::= and
            || ::= or
            !  ::= not (unary)
            !& ::= nand
            !| ::= nor
            ~| ::= xor

\end{verbatim}

The primary BDD expression will have the tag BDD0. All other BDD expression
should have non-zero integer appended to string 'BDD' e.g. BDD1, BDD2 etc.
Any BDD expression can nest other BDD expressions such as BDD1 ::= (or BDD2
BDD3). No BDDX expression is allowed to nest BDD0 as a sub-expression. All
BDD expression must be in reverse-polish notation.

For example, a typical BDD file would look like this. It is left to the
user to specify consistent ordering with BDD subexpressions. However, a
suitable algorithm should be implemented to compute the ordering of the
variables.

\begin{verbatim}
# This is a comment line.
# One should give a variable ordering (optional)
BDD1 ::= (|| x2 x3)
BDD2 ::= (&& (! BDD1) x1)
BDD0 ::= (~| BDD1 BDD2)
\end{verbatim}


\nwenddocs{}\nwbegincode{1}\moddef{IncludesHeaderFiles}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
#include        <stdio.h>
#include        <string.h>
#include        <error.h>
#include        <ctype.h>
#include        <stdlib.h>
#include        <stdarg.h>
#include        "construct_bdd.h"

\nwendcode{}\nwbegindocs{2}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The header file}

Although function definitons and variables declarations are generally
kept in header file, in this literate program,  we use a sigle
{\Tt{}noweb\nwendquote} file to maintain readability. However two files will be
created by {\Tt{}notangle\nwendquote}.  One is a source file and other is a header
file {\Tt{}Header\nwendquote}.

\nwenddocs{}\nwbegincode{3}\moddef{Header}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\LA{}License\RA{}
\LA{}GlobalVariables\RA{}
\LA{}Definition\RA{}
#ifndef CONSTRUCT_BDD_H
#define CONSTRUCT_BDD_H


#endif


\nwendcode{}\nwbegindocs{4}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Definitions}

\nwenddocs{}\nwbegincode{5}\moddef{Definitions}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup

\nwendcode{}\nwbegindocs{6}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Global Variables}
\nwenddocs{}\nwbegincode{7}\moddef{GlobalVariables}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup

\nwendcode{}\nwbegindocs{8}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Functions}

\subsection{Read File}


\nwenddocs{}\nwbegincode{9}\moddef{Functions}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup

\nwendcode{}\nwbegindocs{10}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The main function}
\nwenddocs{}\nwbegincode{11}\moddef{TheMainFunction}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
int main (int argc, char** argv)
\{
    printf("Hello class!\\n");
    return EXIT_SUCCESS;
\}

\nwendcode{}\nwbegindocs{12}\nwdocspar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Structure of the program}
Most of the C programs have a generic structure. 
\nwenddocs{}\nwbegincode{13}\moddef{*}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\LA{}License\RA{}
\LA{}IncludesHeaderFiles\RA{}
\LA{}Functions\RA{}
\LA{}TheMainFunction\RA{}

\nwendcode{}\nwbegindocs{14}\nwdocspar
\section{License and other stuff}
\nwenddocs{}\nwbegincode{15}\moddef{License}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
/* (c) 2011 GNU GPL
 * Dilawar Singh 
 * Email : dilawar@ee.iitb.ac.in
 * Indian Institute of Technology Bombay
 */


\nwendcode{}\end{document}

